This tutorial assumes you know how to construct LC instances; if not, see the tutorial on Constructing LCs. This tutorial covers what it means for a symbol to be free or bound inside an LC tree.

(Each piece of sample code below is written as if it were a script sitting in the root folder of this source code repository, and run from there with the command-line tools node. If you place your scripts in another folder, you will need to adjust the path in each import statement accordingly. If you have not yet set up a copy of this repository with the appropriate Node.js version installed, see our GitHub README, which explains how to do so.)

Free variables vs. free symbols

Most situations that deal with the concepts of free/bound with respect to binding expressions speak of free and bound variables. But in the world of LCs, we do not have variables as a specific category; we have only the general category of symbols that can be used as variables or constants. Thus here we will speak of free and bound symbols.

The concept of a bound variable has the usual meaning: Inside any Binding expression (head sym1 sym2 ... symN , body), the symbols sym1 through symN are bound. Outside of that expression (assuming there is no containing binding expression of the same symbol(s)), they are not bound, and are thus called free.

However, in Lurch, we separate the operator (head in the above example) from the binding itself, so the code written above, (head sym1 sym2 ... symN , body) is equivalent to the more explicit version (head (sym1 sym2 ... symN , body)). The outer expression is a unary application of operator in question (here called head) and the inner expression is a "binding" that is equivalent to body but with several variables now bound.

import { LogicConcept } from './core/src/index.js'

const universalExample = LogicConcept.fromPutdown( '(forall x , (P x))' )[0]
universalExample.descendantsSatisfying( d => d.isAtomic() ).map( d => {
    console.log( 'Is', d.toPutdown(), 'free?', d.isFree() )
} )

// Console output:
Is forall free? true
Is x free? false
Is P free? true
Is x free? false

You can also ask the question relatively: Is a symbol free in a specific ancestor?

const outer = LogicConcept.fromPutdown( '(exists x , (forall y , (> x y)))' )[0]
const inner = outer.child( 1 ).body() // = (forall y , (> x y))
const secondX = inner.child( 1 ).body().child( 1 ) // = (> x y)
console.log( 'Is x free in the inner binding?', secondX.isFree( inner ) )
console.log( 'Is x free in the outer binding?', secondX.isFree( outer ) )

// Console output:
Is x free in the inner binding? true
Is x free in the outer binding? false

The isFree() method works not only for symbols. You can ask whether a nonatomic expression is free, and it will be free if and only if all of the symbols free within it are free in the given context.

// Is the (> x y) free in the (forall y , (> x y)) from above?
console.log( inner.child( 1 ).body().isFree( inner ) )

// Console output:
false

Free occurrences

We can also ask whether a symbol occurs free anywhere in an expression. Note the difference between x.occursFree(y) and y.occursFree(x) and that the order may be different from what you expect.

import { LurchSymbol } from './core/src/index.js'

const example = LogicConcept.fromPutdown( '(and (> x 1) (forall x , (R x x)))' )[0]
console.log( 'Last x free?', example.child( 2 ).child( 1 ).body().child( 2 ).isFree() )
console.log( 'Any x free?', example.occursFree( new LurchSymbol( 'x' ) ) )

// Console output:
Last x free? false
Any x free? true

You can get all free occurrences by combining descendantsSatisfying() with isFree().

Variable capture and replacing free occurrences

The usual notion of variable capture exists when considering substitution into a binding, and you can check to see if it will happen using isFreeToReplace(). You can do all of the free replacements with replaceFree().

console.log( 'Before:', example.toPutdown() )
example.replaceFree(
    new LurchSymbol( 'x' ),
    LogicConcept.fromPutdown( '(- 3 x)' )[0] )
console.log( 'After:', example.toPutdown() )

// Console output:
Before: (and (> x 1) (forall x , (R x x)))
After: (and (> (- 3 x) 1) (forall x , (R x x)))